es:event_system{i:l}, L:(Id List), del:rationals.
fischer{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2}
fischer(es; L)
 (e:es-E(es). 
 f-event{x:ut2}
 f-event(es; L; e)
  (fischer-inv{i:l,
  (fischer-inv{x:ut2,
  (fischer-inv{try:ut2,
  (fischer-inv{taken:ut2,
  (fischer-inv{contending:ut2,
  (fischer-inv{free:ut2,
  (fischer-inv{mine:ut2,
  (fischer-inv{wanted:ut2,
  (fischer-inv{z:ut2}
  (fischer-inv(es; L; del; e)
  ( prop{i:l})) 

latex

Definitions	guard(T), sq_type(T), x. t(x), False, x:A. B(x), A c B, IdLnk, (x  l), P  Q, es-le(es; e; e'), A  B, , A, l_all(L; T; x.P(x)), mkid{$x:ut2}, P  Q, fischer-inv, prop{i:l}, t  T, P  Q, Id, x:A. B(x), x(s), P  Q, es-dtype(es; i; x; T), b, @e(xv), f-newround{$x:ut2, $free:ut2, $mine:ut2}(es; L; e), f-event{$x:ut2}(es; L; e), fischer
Lemmas	event system wf, Id wf, rationals wf, fischer wf, es-E wf, es-time wf, qdist wf, qle wf, inc-snd wf, IdLnk wf, es-isrcv wf, assert wf, es-loc wf, not wf, es-change-to wf, f-rank wf, es-sender wf, es-lnk wf, es-tag wf, f-newround wf, es-locl wf, Id sq, alle-at wf, f-round wf, le wf, f-event wf, existse-at wf, false wf, select wf, length wf1, nat wf, es-after wf